/-
Copyright (c) 2025 Riccardo Brasca. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Riccardo Brasca, Anthony Fernandes, Marc Robin
-/
module

public import Mathlib.Algebra.Module.SpanRank
public import Mathlib.RingTheory.Noetherian.OfPrime
public import Mathlib.RingTheory.PowerSeries.Inverse
public import Mathlib.RingTheory.PowerSeries.Trunc
public import Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

/-!
# Ideals in power series.

We gather miscellaneous results about prime ideals in `R⟦X⟧`. More precisely, we prove that, given
a prime ideal `I` of `R⟦X⟧`, if the ideal generated by the constant coefficients of the `f ∈ I` is
generated by `n` elements, then `I` is generated by at most `n + 1` elements (actually it is
generated by `n` elements if `X ∉ I` and `n + 1` elements otherwise). This implies immediately that
`R⟦X⟧` is noetherian if `R` is. The proof of `eq_of_le_of_X_notMem_of_fg_of_isPrime` is inspired by
[zbMATH05171613].


## Main results

* `PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq` : given an ideal `I` of `R⟦X⟧` such that
  `X ∈ I`, if `I.map constantCoeff` is generated by `S : Set T`, then `I` is generated by
  `insert X (C '' S)`.
* `PowerSeries.exist_eq_span_eq_ncard_of_X_notMem` : given a prime ideal `I` of `R⟦X⟧` such
  that `X ∉ I`, if `I.map constantCoeff` is generated by a finite set `S : Set T`, then there exists
  `T : Set R`, of the same cardinality as `S`, that generates `I`.
* `PowerSeries.fg_iff_of_isPrime` : a prime ideal `P` of `R⟦X⟧` is finitely generated if and only
  if `P.map constantCoeff` is finitely generated.


## Implementation details

There is a simpler proof of `IsNoetherianRing R → IsNoetherianRing R⟦X⟧`, similar to that for
polynomials. On the other hand our proof has the advantage of giving explicitly the number of
generators, and it is used to prove that, for a domain `R`, we have
`IsPrincipalIdealRing R → UniqueFactorizationMonoid R⟦X⟧`.

## TODO
Prove noetherianity of `MvPowerSeries` in finitely many variables.

-/

@[expose] public section

variable {R : Type*}

open Ideal Set Finset

namespace PowerSeries
variable [CommRing R] {I : Ideal R⟦X⟧} {S : Set R}

section X_mem

theorem map_constantCoeff_le_self_of_X_mem (hXI : X ∈ I) :
    I.map (C.comp constantCoeff) ≤ I := by
  suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]
  intro f hf
  rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]
  exact sub_mem hf (I.mul_mem_right _ hXI)

/-- Given an ideal `I` of `R⟦X⟧` such that `X ∈ I`, if `I.map constantCoeff` is generated by
`S : Set T`, then `I` is generated by `insert X (C '' S)`. -/
theorem eq_span_insert_X_of_X_mem_of_span_eq (hXI : X ∈ I) (hSI : span S = I.map constantCoeff) :
    I = span (insert X (C '' S)) := by
  rw [Ideal.span_insert, ← Ideal.map_span, hSI, Ideal.map_map]
  refine le_antisymm ?_ (by simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem])
  exact fun f hf ↦ mem_span_singleton_sup.mpr
    ⟨_, _, mem_map_of_mem _ hf, f.eq_shift_mul_X_add_const.symm⟩

open Submodule in
theorem spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem (hI : X ∈ I) :
    spanFinrank I ≤ spanFinrank (I.map constantCoeff) + 1 := by
  by_cases hfg : I.FG
  swap; · exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _
  replace hfg : (Ideal.map constantCoeff I).FG := by
    have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
    exact map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg
  nth_rw 1 [eq_span_insert_X_of_X_mem_of_span_eq hI (I.map constantCoeff).span_generators]
  refine le_trans (spanFinrank_span_le_ncard_of_finite ?_) (le_trans (Set.ncard_insert_le _ _) ?_)
  · simpa using Set.Finite.map _ (FG.finite_generators hfg)
  · simp only [add_le_add_iff_right]
    refine le_trans (Set.ncard_image_le (FG.finite_generators hfg)) ?_
    rw [FG.generators_ncard hfg]

end X_mem

section X_notMem

variable (hXI : X ∉ I) [I.IsPrime]

theorem eq_of_le_of_X_notMem_of_fg_of_isPrime {J : Ideal R⟦X⟧} (hJI : J ≤ I) (hXI : X ∉ I)
    (hJ : J.FG) (h' : I.map constantCoeff ≤ J.map constantCoeff) : I = J := by
  refine hJI.antisymm' ?_
  replace h' := h'.antisymm (Ideal.map_mono hJI)
  obtain ⟨n, F, rfl⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hJ
  rw [submodule_span_eq, map_span, ← Set.range_comp] at h'
  choose! T hT using fun g (hg : g ∈ I) ↦
    mem_span_range_iff_exists_fun.mp (h'.le (Ideal.mem_map_of_mem _ hg))
  dsimp at hT
  intro g hg
  let G : ℕ → R⟦X⟧ :=
    Nat.rec g fun _ G' ↦ mk fun p ↦ coeff (p + 1) G' - ∑ i, T G' i * coeff (p + 1) (F i)
  have hG' (n : ℕ) (H : G n ∈ I) : G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1) := by
    simpa [hT _ H] using sub_const_eq_X_mul_shift (G n - ∑ i, C (T (G n) i) * F i)
  have hG : ∀ n, G n ∈ I := Nat.rec hg fun n IH ↦
    (‹I.IsPrime›.mul_mem_iff_mem_or_mem.mp (hG' n IH ▸ I.sub_mem IH (I.sum_mem fun i _ ↦
      I.mul_mem_left _ (hJI (subset_span (Set.mem_range_self _)))))).resolve_left hXI
  replace hG' := fun n ↦ hG' n (hG n)
  let H (i : Fin n) : R⟦X⟧ := mk fun n ↦ T (G n) i
  have h₁ (n : ℕ) : g - ∑ i, trunc n (H i) * F i = X ^ n * G n := by
    induction n with
    | zero => simp [G]
    | succ n IH =>
      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]
  have h₂ : g = ∑ i, H i * F i := by
    ext n; simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)
  rw [h₂]
  exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _ (subset_span (Set.mem_range_self _))

/-- Given a prime ideal `I` of `R⟦X⟧` such that `X ∉ I`, if `I.map constantCoeff` is generated by a
finite set `S : Set T`, then there exists `T : Set R`, of the same cardinality as `S`, that
generates `I`. -/
theorem exist_eq_span_eq_ncard_of_X_notMem (hI : X ∉ I) {S : Set R}
    (hSI : span S = I.map constantCoeff) (hS : S.Finite) :
      ∃ T, I = span T ∧ T.Finite ∧ T.ncard = S.ncard := by
  have : SurjOn constantCoeff I S := by
    intro r hr
    simpa [mem_map_iff_of_surjective _ constantCoeff_surj, hSI] using subset_span hr
  obtain ⟨T, hTI, hinj, hT⟩ := this.exists_subset_injOn_image_eq
  refine ⟨T, eq_of_le_of_X_notMem_of_fg_of_isPrime (span_le.2  hTI) hI (Submodule.fg_def.2
    ⟨T, (hT ▸ hS).of_finite_image hinj, rfl⟩) ?_, Finite.of_injOn
    (fun f hf ↦ hT ▸ Set.mem_image_of_mem _ hf) hinj hS, hT ▸ (ncard_image_of_injOn hinj).symm⟩
  rw [map_le_iff_le_comap]
  intro f hf
  rw [mem_comap, mem_map_iff_of_surjective _ constantCoeff_surj]
  replace hf : constantCoeff f ∈ span S := hSI ▸ Ideal.mem_map_of_mem constantCoeff hf
  refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
  · obtain ⟨t, htmem, ht⟩ := hT ▸ hs
    exact ⟨t, subset_span htmem, ht⟩
  · intro r₁ r₂ hr₁ hr₂ ⟨s₁, hs₁mem, hs₁⟩ ⟨s₂, hs₂mem, hs₂⟩
    exact ⟨s₁ + s₂, Ideal.add_mem _ hs₁mem hs₂mem, by simp [hs₁, hs₂]⟩
  · intro r₁ r₂ hr₁ ⟨f, hfmem, hf⟩
    exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩

open Submodule in
theorem spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime (hI : X ∉ I)
    (hfg : I.FG) : spanFinrank I = spanFinrank (I.map constantCoeff) := by
  refine le_antisymm ?_ ?_
  swap; · exact Ideal.spanFinrank_map_le_of_fg constantCoeff hfg
  have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
  obtain ⟨S, rfl, hS, hScard⟩ := exist_eq_span_eq_ncard_of_X_notMem hI
    (I.map constantCoeff).span_generators
    (FG.finite_generators <| map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg)
  refine le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_
  rw [hScard, FG.generators_ncard]
  exact map_eq_submodule_map constantCoeff (Ideal.span S) ▸ Submodule.FG.map _ hfg

end X_notMem

variable {P : Ideal R⟦X⟧} [P.IsPrime]

open Submodule in
theorem spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime :
    spanFinrank P ≤ spanFinrank (P.map constantCoeff) + 1 := by
  by_cases hfg : P.FG
  swap; · exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _
  by_cases hP : X ∈ P
  · exact spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem hP
  · exact le_trans (spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime
      hP hfg).le (Nat.le_succ _)

/-- A prime ideal `P` of `R⟦X⟧` is finitely generated if and only if `P.map constantCoeff` is
finitely generated. -/
lemma fg_iff_of_isPrime : P.FG ↔ (P.map constantCoeff).FG := by
  constructor
  · exact (FG.map · _)
  · intro ⟨S, hS⟩
    by_cases hX : X ∈ P
    · have H := eq_span_insert_X_of_X_mem_of_span_eq hX hS
      have : (insert X <| (C (R := R)) '' S).Finite :=
        Finite.insert X <| Finite.image _ S.finite_toSet
      lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT
      exact ⟨T, hT ▸ H.symm⟩
    · obtain ⟨T, hT, hT₂, _⟩ := exist_eq_span_eq_ncard_of_X_notMem hX hS S.finite_toSet
      lift T to Finset R⟦X⟧ using hT₂
      exact ⟨T, hT.symm⟩

/-- If `R` is noetherian then so is `R⟦X⟧`. -/
instance [IsNoetherianRing R] : IsNoetherianRing R⟦X⟧ :=
  IsNoetherianRing.of_prime fun P _ ↦
    fg_iff_of_isPrime.2 <| (isNoetherianRing_iff_ideal_fg R).1 inferInstance (P.map constantCoeff)

/-- If `R` is principal then `R⟦X⟧` is a `UniqueFactorizationMonoid`. Note that `R` being a
`UniqueFactorizationMonoid` is not enough. -/
instance [IsPrincipalIdealRing R] [IsDomain R] : UniqueFactorizationMonoid R⟦X⟧ := by
  refine UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)
  by_cases hXP : X ∈ P
  · exact ⟨X, hXP, X_prime⟩
  · obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal
    obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)
    simp only [ncard_singleton, ncard_eq_one] at h
    obtain ⟨_, rfl⟩ := h
    exact ⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩

end PowerSeries
